Skip to content

SMT2 back-end: flatten with_exprt operands #8670

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 3 commits into from
Jul 23, 2025
Merged

SMT2 back-end: flatten with_exprt operands #8670

merged 3 commits into from
Jul 23, 2025

Conversation

tautschnig
Copy link
Collaborator

Solvers without datatypes support require flattening towards bitvectors. This is also true for array-typed expressions when the array is not at the top level (despite possible array-theory support). This changes makes sure we will flatten such array-typed expressions.

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@tautschnig tautschnig mentioned this pull request Jul 2, 2025
Open
@codecov Codecov
Copy link

codecov bot commented Jul 2, 2025 •
edited
Loading

Codecov Report

Attention: Patch coverage is 66.66667% with 14 lines in your changes missing coverage. Please review.

Project coverage is 80.39%. Comparing base (062962c) to head (769f7a2).
Report is 4 commits behind head on develop.

Files with missing lines Patch % Lines
src/solvers/smt2/smt2_conv.cpp 66.66% 14 Missing ⚠️
Additional details and impacted files 
@@           Coverage Diff            @@
##           develop    #8670   +/-   ##
========================================
  Coverage    80.39%   80.39%           
========================================
  Files         1688     1688           
  Lines       207383   207402   +19     
  Branches        73       73           
========================================
+ Hits        166731   166748   +17     
- Misses       40652    40654    +2

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
  • 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

@tautschnig tautschnig self-assigned this Jul 9, 2025
@tautschnig
Copy link
Collaborator Author

tautschnig commented Jul 9, 2025 •
edited
Loading

Note to reviewers: #8637 includes a test set-up with tests passing once the changes in this PR are applied. I am working on extracting a minified variant thereof to include as regression test. Edit: done.

@tautschnig tautschnig force-pushed the convert-with branch 2 times, most recently from 016dcc1 to 6edd58a Compare July 16, 2025 10:02
@tautschnig tautschnig requested a review from a team as a code owner July 16, 2025 10:02
@tautschnig
CI: Make smt2_solver available to all regression tests
9611331 
We will want to use the solver for more than just selected CBMC
regressions.
@tautschnig
SMT2 back-end: flatten with_exprt operands
9a1df4b 
Solvers without datatypes support require flattening towards bitvectors.
This is also true for array-typed expressions when the array is not at
the top level (despite possible array-theory support). This changes
makes sure we will flatten such array-typed expressions.
@tautschnig tautschnig mentioned this pull request Jul 20, 2025
Open
@rod-chapman
Copy link
Collaborator

This branch does seems to fix the array flattening issue on the mlda-native code when using bitwuzla.

TWO functions still fail with a different error though. For example, the unpack-hints function in mldsa-native:

cbmc --bitwuzla --outfile b.smt2 gotos/unpack_hints_harness.goto
bitwuzla b.smt2

yields

[error] b.smt2:18036:529: expected terms of same sort at indices 1 and 2 as argument to 'ite'

Is this related, or a completely different problem?

@tautschnig
Copy link
Collaborator Author

Thank you for testing! I'll take a look tomorrow morning to figure out whether the remaining problem (besides unpack_hints, which is the other function that still is having issues?) is unrelated or the proposed bugfix is incomplete.

@rod-chapman
Copy link
Collaborator

Results: testing with CBMC (this branch), Z4 4.12.6 and Bitwuzla 0.7.0 on the mldsa-native, HEAD of main branch - all 134 functions/proofs OK.

@rod-chapman
Copy link
Collaborator

Testing this branch (with 3rd commit) on mlkem-native main/HEAD - all 126 proofs OK.

@rod-chapman
Copy link
Collaborator

Testing this branch (with 3rd commit) on mldsa-native - 134 proofs all OK, and a bit faster too.

@tautschnig
SMT2 back-end: ite-conversion must uphold type consistency
769f7a2 
WITH expressions in an ite expression could previously trigger
one-sided expression flattening.
@tautschnig tautschnig assigned TGWDB and unassigned tautschnig and kroening Jul 23, 2025
@tautschnig tautschnig merged commit dc193c4 into diffblue:develop Jul 23, 2025
39 of 41 checks passed
@tautschnig tautschnig deleted the convert-with branch July 23, 2025 22:35
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kroening kroening kroening approved these changes

@TGWDB TGWDB TGWDB approved these changes

@martin-cs martin-cs Awaiting requested review from martin-cs martin-cs is a code owner

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

Assignees

@peterschrammel peterschrammel

@TGWDB TGWDB

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@tautschnig @rod-chapman @kroening @TGWDB @peterschrammel